// Copyright 2011 Google Inc. All Rights Reserved.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

open websec

sig HTTPAuth extends Auth {
  // Origin includes a schema and a dnslabel (port is commented out in weblib?)
  host: one Origin
} {
  // BCAP specifies https
  host.schema = HTTPS
}

sig PathOpaque extends Opaque { path: one Path }

// ResourceCaps model implementations that return data only, no caps
sig HTTPResourceCap extends Cap { }
{
	all cs: CapServer, c: Cap | cs.impls[opaque].invoke[c] = none
}

// All PathOpaques point to distinct paths
fact {
  all disj pathO1, pathO2: PathOpaque | pathO1.path != pathO2.path
}

sig CapPrincipal extends WebPrincipal {
  capServer: one CapServer // just one for now?
}

sig HTTPCapServer extends HTTPServer {
  capServer: one CapServer
}

sig BelayServer extends HTTPCapServer {}
sig ParanoidBelayServer extends BelayServer {}
sig OpenBelayServer extends BelayServer {}

fun requestCaps[r: HTTPRequest]:set Cap {
  r.body.tokenCaps + r.headers.headerCaps + r.queryString.(name + value).tokenCaps
}

fun responseCaps[r: HTTPResponse]:set Cap {
  r.body.tokenCaps + r.headers.headerCaps
}

fact canOnlySendCapsYouKnowAbout {
  all server: NetworkEndpoint, rq: HTTPRequest, rp: HTTPResponse, cap: Cap {
      (rq.from = server and (cap in requestCaps[rq])) implies capsKnownByServer[cap, server, rq]
      (rp.from = server and (cap in responseCaps[rp])) implies capsKnownByServer[cap, server, rp]
  }
}

fact belayServersOnlyGetCapsFromBody {
  all server:BelayServer, cs:Cap, event:Event {
    capsKnownByServer[cs, server, event] implies
    (some r:HTTPRequest { r.to = server and cs in r.body.tokenCaps })
    or
    (some r:HTTPResponse { r.to = server and cs in r.body.tokenCaps })
  }
}

fact belayServersRespondWithImplementationCaps {
  all t:HTTPTransaction,
      server: BelayServer,
      server': HTTPCapServer,
      c: Cap {
    httpCapInvoke[c, server, server', t] implies
    // The response matches the implementation
    responseCaps[t.resp] in ((server'.capServer.impls)[c.opaque]).invoke[requestCaps[t.req]]
  }
}

// Assumes the BelayServer only talks outwardly to other
// ParanoidBelayServer
fact belayServersTalkToBelayServers {
  all server:ParanoidBelayServer, ne:NetworkEvent {
    ne.from = server implies some server':ParanoidBelayServer, c:Cap, t:HTTPTransaction {
      ne.to = server' and httpCapInvoke[c, server, server', t]
    }
  }
}

fact openBelayServersTalkWithInvokes {
  all server:OpenBelayServer, ne:NetworkEvent {
    ne.from = server implies
      some server':HTTPCapServer, c:Cap, t:HTTPTransaction {
        ne.to = server' and httpCapInvoke[c, server, server', t]
      }
  }
}

// Does this Server know about these caps?
pred capsKnownByServer[cs: set Cap, server: NetworkEndpoint, event: Event] {
  all c:cs {
    (some r:HTTPRequest {
      happensBeforeOrdering[r, event] and r.to = server and c in (requestCaps[r])
    }) or
    (some r:HTTPResponse {
      happensBeforeOrdering[r, event] and r.to = server and c in (responseCaps[r])
    }) or
    // Weird condition:  Only works for network endpoints with capServers
    cs in server.capServer.caps
  }
}

//run {some cs:Cap, server: NetworkEndpoint, event: Event | capsKnownByServer[cs, server, event] }

pred httpCapInvoke[c: Cap, s1:NetworkEndpoint, s2: HTTPCapServer, t:HTTPTransaction] {
  c.opaque in PathOpaque
  c.auth in HTTPAuth // this is what makes it a 'httpcap'
  c in s1.capServer.caps
  t.req.from = s1 and t.req.to = s2
  t.req.path = c.opaque.path
  t.req.method in GET + PUT + POST + DELETE
  t.req.host = c.auth.host
}

pred capsStayInParanoidServersPrecondition[cs:Cap, s1, s2:ParanoidBelayServer, t:HTTPTransaction] {
    (all s:NetworkEndpoint - s1 { not capsKnownByServer[cs, s, t.req] })
    and (all s:NetworkEndpoint - (s1 + s2) { not (s in ParanoidBelayServer) })
    and capsKnownByServer[cs, s1, t.req]
    and httpCapInvoke[cs, s1, s2, t]
}

//run capsStayInParanoidServersPrecondition for 5

assert capsStayInParanoidServers {
  all s1,s2: ParanoidBelayServer, cs: Cap, t:HTTPTransaction {
    // Cap is *only* known to s1 at the time of the request
    (all sNotKnownToStart:NetworkEndpoint - s1 {
      not capsKnownByServer[cs, sNotKnownToStart, t.req]
    }) and
    // Nothing else in the world is a ParanoidBelayServer
    (all sNonBelayServer:NetworkEndpoint - (s1 + s2) {
      not (sNonBelayServer in ParanoidBelayServer)
    }) and
    // One of the ParanoidBelayServer knows about the cap to start
    capsKnownByServer[cs, s1, t.req] and
    // And it invokes the cap at s2 (implies that the cs
    // implementation is on s2)
    httpCapInvoke[cs, s1, s2, t]
    implies
    // At every future event, all the other servers don't know about cs
    all sNotKnownLater:NetworkEndpoint - (s1 + s2), event:Event {
      not capsKnownByServer[cs, sNotKnownLater, event]
    }
  }
}

assert leakingResourceCapOnlyLeaksThatCap {
  all s1:OpenBelayServer, s2:NetworkEndpoint - BelayServer, c:HTTPResourceCap {
    c in s1.capServer.caps
    implies
    (all event:Event, c':Cap - c {
      capsKnownByServer[c, s2, event.next]
      and (not some s3:NetworkEndpoint - s1 | capsKnownByServer[c', s3, event.next])
      implies
      (all event':Event - event {
        happensBeforeOrdering[event, event']
        implies not capsKnownByServer[c', s2, event']
      })
    })
  }
}

// check leakingResourceCapOnlyLeaksThatCap for 8

/*
// All the capabilities that a given network endpoint can reach
pred capsReachable[reachables: set Cap, server: NetworkEndpoint, event: Event] {
  all reachable: reachables, cs:Cap {
    capsKnownByServer[cs, server, event] implies
    reachable in cs or
    some 
  }
}
*/

check capsStayInParanoidServers for 8


run httpCapInvoke for 5 


// An implementation takes some caps as arguments, and returns a new set of caps
sig Implementation { invoke: set Cap -> set Cap }
sig PublicIface { }

sig CapServer {
  auth: one Auth,
  publicInterface: one PublicIface,
  caps: set Cap,
  impls: Opaque lone->lone Implementation,
  resolver: Auth lone->lone PublicIface
}

fact {
  all cs,cs':CapServer, o:Opaque, i:Implementation {
    (cs != cs' and i = cs.impls[o]) implies (not some i':Implementation | i' in cs'.impls[o])
  }
}

fact {
  all cs:CapServer, a:Auth | cs.publicInterface not in cs.resolver[a]
}

fact {
  all cs, cs':CapServer | cs != cs' implies cs.publicInterface != cs'.publicInterface
}

// An implementation lives within a single capserver (some kind of isolation assumption?)
fact {
  all cs, cs':CapServer, i:Implementation, o:Opaque | (cs != cs' and i in cs.impls[o]) implies not (i in cs'.impls[o])
}

// Caps always exist within a capserver?
fact {
  all c:Cap | (some cs:CapServer | c in cs.caps)
}

assert noServerLoop {
  all cs:CapServer, a:Auth | cs.resolver[a] != cs.publicInterface
}

pred invocable [cs:CapServer, c:Cap] {
  some i:Implementation | i= cs.impls[c.opaque]
}

pred reachable [cs,cs':CapServer, c:Cap]  {
  // an invocable capserver is reachable through some chain of resolvers
  cs'.publicInterface in c.auth.*(cs.resolver) and invocable[cs', c]
  or invocable[cs, c]
}

// Only one cap server has an implementation for c's opaque
assert invocableInOnePlace {
  all cs:CapServer, c:Cap | (invocable[cs, c] implies (not some cs':CapServer | cs != cs' and invocable[cs', c]))
}


pred grant [cs, cs':CapServer, c:Cap, i:Implementation, a:Auth] {
  cs != cs' and
  (all cs'':CapServer | cs'' != cs' implies c not in cs''.caps) and
  (c in cs'.caps and c.auth = a) and
  (cs'.impls[c.opaque] = i)
}

assert grantSafe {
  all cs,cs':CapServer, i:Implementation, a:Auth, c:Cap {
    grant[cs,cs', c, i, a] implies
    (all cs'':CapServer | cs'' != cs' implies c not in cs''.caps)
  }
}

// c is invoked from cs, with an implementation for its opaque in cs',
// which results in cs' changing to cs'', which has new caps
pred invoke[cs,cs',cs'':CapServer, c:Cap, args:set Cap] {
  c in cs.caps and
  args in cs.caps and
  reachable[cs, cs', c] and
  cs'.publicInterface = cs''.publicInterface and
  cs'.impls = cs''.impls and
  cs'.resolver = cs''.resolver and
  cs''.caps = cs'.caps + args
}

// An auth only takes you to one place
assert uniqueAuth {
  all cs,cs':CapServer, c:Cap {
    ((cs != cs' and reachable[cs, cs', c]) implies 
       (all cs'':CapServer | cs' != cs'' and cs != cs'' implies not reachable[cs, cs'', c]))
    or
    (cs != cs' and invocable[cs, c]  and not (some cs'':CapServer | cs'' != cs and reachable[cs', cs'', c]))
  }
}

check uniqueAuth for 5
check grantSafe
check invocableInOnePlace for 5
check noServerLoop for 5

run grant for 5
run reachable for 3
run invocable

// Are all browser caps reachable? (No, not back from the web server)
// Can we partition stations to show that some caps *can't* be invoked from certain places?
// Two caps pointing to the same implementation?
// Auths are globally unique?  Every resolver with an entry for an Auth gives the same answer?  false...
//     - What about every auth will either be unreachable or find a unique CapServer?  Then you can't replicate
// One page can only invoke a JavaScript implementation on another page via:
//     - getting it through a user action initiated transfer, and routing through station
//     - backend collusion
//     - if the capserver wraps everything, then they really can't do this!
// What if a CapServer mints with the wrong Auth?
//    - unintelligible caps at the other side (Opaque is unguessable)
//    - things that rely on introduction might be in trouble
